1. Technical Field
The present invention relates to an improved method for verifying designs and, in particular, to a method of formal verification which provides the user with a simple method of extracting the desired data.
2. Description of Related Art
Designers and inventors have long sought methods of confirming their designs without actually building the design in physical form and using trial and error. With the advent of computers, simulation has become and still is the most common hardware verification framework in use today. Simulation requires that a battery of tests be run through a model of the implementation of a particular design, trying out a number of possible input variations, and then checking to see that the model meets the specifications. Simulation consists of the application of an ordered sequence of input vectors to a particular model that is being tested.
Simulation is polynomial in complexity with respect to the model being tested. However, for complex designs, the amount of behavioral coverage obtainable through simulation decreases rapidly. As designs become more complex, simulation becomes very inefficient in verifying the design. Hence, simulation cannot be done exhaustively even for moderately large designs.
Recently, there has been increased interest in formal verification methods. In formal verification methods, mathematical reasoning frameworks are implemented which exhaustively cover the design behavior. The method consists of using formal proofs to verify that a design satisfies certain properties, which are sometimes referred to as formal specifications.
While the algorithms used in formal verification methods tend to be exponential in complexity with respect to the design size, the results in the hands of skilled users have proven its utility. Symbolic model checking is a type of formal verification and is now a common part of the design validation process. Model checking is a fully automated technique which verifies that a set of properties specified with temporal formulas will hold for a given design.
Referring now to FIG. 1, algorithm 100 for such a technique requires a formal description of design environment 120. That is, a definition of the conditions to which the design under test is to be subjected must be provided to the algorithm. The algorithm also requires a description of the hardware itself, called the model 110, and a property 130 that is to be verified by algorithm 135. Once environment 120, model 110, and property 130 are input, a determination is made by algorithm 135 as to whether property 130 passes or fails at block 140.
In addition to a xe2x80x9cpass or failxe2x80x9d result, a cycle-by-cycle trace of all signal values illustrating a counter-example is typically provided at block 150 upon a failure. A counter-example is a stream of execution which violates the specified property. Also, a trace illustrating a witness is typically provided at block 160 upon a pass. A witness is a stream of execution which non-trivially satisfies the specified property.
For example, if the property is xe2x80x9cif REQ is active, then GNT must be active in 3 cycles,xe2x80x9d a nontrivial stream of execution which satisfies this property is one which shows that the request REQ becomes active. If so, then the grant GNT will be checked in three cycles, and if it is not active, then the property will fail. An example of a stream of execution which trivially satisfies the property is the case in which REQ never occurs. Thus, there will be no opportunity for the property to fail, and hence no meaningful trace to display.
In order to generate these traces, the model checker arbitrarily calculates a set of valuations of the state variables in the model which comprise only one possible witness or counter-example. If the user is happy with the trace that was generated by the model checker, then the model checking procedure is finished at block 170. However, if the user is not satisfied with the trace that was generated, either model 110 or environment 120 is modified in order to get a more satisfactory trace for property 130.
The complexity of model checking is also exponential in relation to the size of the model, the environment, and the property to be tested. The reason for this is that the modeling technique or tool performs a breadth-first exhaustive reachability calculation. That is, beginning with all initial states, all states reachable in one xe2x80x9csimulation stepxe2x80x9d(denoted Image 1) are explored. Then, all states reachable in two simulation steps (denoted Image 2) are explored, and so on until no new states are found. One reason that breadth-first algorithms are typically used rather than depth-first algorithms is to avoid excessively long traces if the error could manifest itself in a shorter period of time using a breadth-first algorithm.
One shortcoming of formal verification techniques is the xe2x80x9cstate-space explosion.xe2x80x9d This problem is seen as the number of state variables in a model is increased. The number of states in a model with N state variables may equal 2N. Thus, as the number of state variables is increased, the complexity of the model increases exponentially. Therefore, such a formal verification method has limited application in industrial designs because of the complexity that usually exists in industrial designs.
Model checkers typically support the notion of the xe2x80x9cinvariantxe2x80x9d or xe2x80x9cinvarxe2x80x9d keyword, whose arguments are a set of Boolean properties. For example, using the command xe2x80x9cinvar pxe2x80x9d truncates the state space exploration of the tool to only consider those states where xe2x80x9cpxe2x80x9d is true. All encountered states where p is not true are discarded along with their successors, generally. (Note that some of the successors will not be discarded if they are encountered along a different path where xe2x80x9cpxe2x80x9d is always true.) Because certain states and paths are ignored due to the invariants, the complexity of the model checking run is thereby reduced.
Imposing cycle-specific restrictions using traditional model checking tools requires the user to manually generate an automaton to count cycles and create standard invariants of the form xe2x80x9cinvar (automata=1)xe2x86x92(REQ=1)xe2x80x9d, xe2x80x9cinvar (automata=2)xe2x86x92(GNT=0)xe2x80x9d, etc. The use of an automaton in this manner creates additional state variables causing even more of a state-space explosion. The additional complexity of the extra automaton may outweigh the benefit of the use of such invariants. The verification tool in many cases consumes more CPU time/memory than in the original run where the automaton was not used. This manual and computational complexity is suffered merely to generate one tailored trace.
An automaton is a finite state machine (FSM). It is a state transition system that consists of a set of states, and a set of transitions defined from one state to the next. For example, consider the array  less than S, I, T greater than  where S is the set of states, I is the set of inputs to the automaton, and T is the transition function. Intuitively, a Finite State Machine (FSM) or an automaton starts in an xe2x80x9cinitial state.xe2x80x9d From its present state, under control of the present input, T defines the next state to which the automaton will transition.
As noted earlier, formal verification (such as model checking) is roughly exponential in relation to the size of the model. Using the prior art, if a trace is obtained which is undesirable, the designer typically couples onto the model under test an automaton which does nothing more than count cycles. A set of user-defined cycle-specific invariants (as above) are then introduced to guide the state space search. This automaton initializes to count=0. Each transition increments its value by one. The implication is that with the automaton added, model checking becomes exponential in relation to the size of the model PLUS the size of the automaton. While the invariants prune the state space search, the constrained run is typically even more costly than the original unconstrained run due to the extra automaton.
Furthermore, because the trace selected by the tool is arbitrary, the problem of the case in which the selected trace is illegal, that is resulting from illegal input behavior, is encountered. To avoid these frequent illegal trace selections, the verification engineer must go to great lengths to specify the environment and property composition that forces the model checker to produce a different and hopefully more attractive trace. This frequently involves very complicated logic and reasoning which is often as complex as the model itself, and in many cases requires a larger composed model, environment, or property composition resulting in an even greater state-space explosion.
To solve this problem, multiple distinct environments are used. One small environment is used for normal xe2x80x9cfastxe2x80x9d property evaluation and then another typically larger environment is used for the xe2x80x9cattractive trace generation.xe2x80x9d The size of the environment is determined by the number of state variables needed to express the environment. Nevertheless, the arrival at such a good set of environments or traces often requires a very sophisticated trial and error refinement process which unnecessarily delays the generation of a good trace and adds undesirable manual and computational complexity. The use of multiple distinct environments is time-consuming because in many cases it requires superfluous full-blown model checking runs in which the model checker must be run again for each modification of the environment and/or property.
Under the current art, the complexity and sophistication required to perform formal verification often requires dedicated verification engineers, and much back-and-forth interaction as necessary between the verification engineer and the designer to obtain desired traces, and to fully enumerate necessary assumptions.
Therefore, there is a need for an extensible tool set and efficient underlying algorithm for achieving the goal of extracting a xe2x80x9cgood tracexe2x80x9d more efficiently with less computational and manual complexity. The user should be able to extract much information very quickly from the tool rather than obtaining an arbitrary trace which may or may not be very desirable. The user should be able to pose questions in a very simple manner and extract traces from the verification tool without extensive trial and error refinement of the trace.
The user should also be able to use the model checker without having an understanding of the underlying algorithm or methods used by the tool. The method should allow the user to do additional tests on the model in an intuitive manner without having to conduct a full-blown model checking run for each modification.
A tool is needed to allow the verification engineer to more efficiently extract necessary assumptions, and to allow the designer to use the traces that were generated by the verification engineer to pose straightforward queries to further the design effort without further intervention by the verification engineer.
The present invention solves the problems of the prior art by making the model checking tool less complex, more efficient, and more user friendly. A waveform based xe2x80x9cinput/outputxe2x80x9d graphical user interface (GUI) is used to allow the user to highlight specific values at specific cycles and to modify the waveform displayed.
The user may begin either from xe2x80x9cscratchxe2x80x9d or from an existing trace produced by the tool. The user makes any changes to the desired waveform that is displayed on the GUI. The resulting waveform represents the trace that the user wishes to extract from the model using the verification tool.
In addition, the present invention allows the user to perform boolean functions over certain signals. The arguments for the function can either be particular values or may relate to temporal constraints such that the time for a particular value is specified.
Once the desired waveform is completed and highlighted, queries using trace tailor are performed. Sufficient modifications of the environment and/or property are made based on the results obtained. To insure that the result obtained is merely an alternate trace of the same pass/fail that was originally obtained, the same model, environment, and property is passed to the model checker. The annotations that are input by the user are translated to xe2x80x9ccycle-specific invariantsxe2x80x9d to force the tool to produce a trace that satisfies the desired annotated waveform and to insure a much faster and more efficient query.
After a trace is provided, the user determines whether or not the trace is satisfactory. If not, then the user may tailor the trace by adding additional constraints to the waveform using the graphic user interface. In the case that the verification tool cannot provide a trace which satisfies the constraints input by the user, the user may make an additional iteration in which he removes one or more of the constraints.
The model checker of the present invention is useful for efficiently enumerating all assumptions necessary for satisfaction of a particular property. In obtaining rigorous proofs, the model checker generates an initial trace, a series of efficient queries using the trace tailor, a sufficient modification of environments and/or properties based on the necessary assumptions obtained from the trace tailor, and a new unrestricted call to the model checker to insure that no failures occur at a particular cycle. The model checker is also useful in conjunction with a rigorous proof approach, not just to enumerate assumptions, but also to merely tailor the traces to make them more succinct, e.g., to more clearly illustrate an error to a designer.
Finally, the trace tailor method may be used in and of itself to fabricate a trace from scratch. The iterative process with the trace tailor when creating the trace from scratch will still yield much information about the behavior of the model under test.
The foregoing techniques may be easily integrated into existing verification tools. The tool set also provides an intuitive and efficient platform for bridging model checking, directed search, and simulation reachability engines, thereby allowing users to obtain desired traces with minimal manual and computational complexity. This tool set helps bridge the gap between formal verification and the designer.